Verified Choreographic Compilers
Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that defines the roles of the participants involved and how they should work together. Through endoint projection, such a choreography can be translated into a separate program for each role. By defining a global plan involving all participants, inconsistencies of otherwise disjoint applications are impossible to write down. This promises to eliminate some common programming errors, such as deadlocks, by design.
Verified compilation, as demonstrated in the CakeML project, means that the entire compilation process from source ML code to machine code is accompanied by a machine-checked proof of correctness. CakeML’s compiler is formally verified, ensuring that the semantics of the source program are preserved at every compilation stage. This approach allows any property proved about the source code to be transported down to the generated machine code, providing strong end-to-end guarantees about program behavior.
Goals
In this seminar, you will become familiar with the concepts of verified compilation, and explore how these concepts are applied to verify the choreographic Kalas compiler.